| Definitions | t  T, f(a),  x:A. B(x), kind(e), Knd, (x l), loc(e), Id, x:A  B(x),  , P & Q, e  X,  b, Type, x:A  B(x), P   Q, E,  x:A. B(x), AbsInterface(A), Top, left + right, ES, s = t, finite-type(T), X is finite, a:A fp B(a), MaInterface(T), ma-interface-consistent-at(es;i;X), ma-interface-consistent(es;X), [[X]], IdDeq, x dom(f), A c B, {x:A| B(x)} , State(ds), hasloc(k;i),   x. t(x), type List, s ~ t, {T}, SQType(T), X is local, t.2, kindtype(i;k), <a, b>, x.A(x), filter(P;l), vartype(i;x), t.1, f(x), f(x)?z, state@i|xs, a < b, Atom$n, S  T, if b then t else f fi , suptype(S; T),  , Unit, ff, tt, IdLnk, act(k), es-V(es), tag(k), lnk(k), es-M(es), case b of inl(x) => s(x) | inr(y) => t(y), deq-member(eq;x;L), strong-subtype(A;B), EqDecider(T), KindDeq, e@i. P(e), False,  A, EOrderAxioms(E; pred?; info), EState(T), kindcase(k; a.f(a); l,t.g(l;t) ), Msg(M),  ,  , val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), e < e', r  s, constant_function(f;A;B), let x,y = A in B(x;y), Void,  x:A.B(x), b, P  Q, valtype(e), P Q, a = b, rcv(l,tg), locl(a), ma-interface-val(es;X;e), ma-in-interface(es;X;e), val(e), state@i, (state when e), P  Q, True, p q,  T, Dec(P), can-apply(f;x), inr x |
| Lemmas | pi2 wf, equal-top, member filter, es-hasloc, decidable assert, assert of band, and functionality wrt iff, squash wf, true wf, bnot thru band, assert of bor, or functionality wrt iff, bor wf, es-state-when wf, es-val wf, es-state-subtype-partial-state, Id sq, Knd sq, es-valtype-kindtype, es-M wf, es-V wf, locl wf, rcv wf, assert-eq-id, assert-eq-knd, pi1 wf, es-partial-state wf, es-kindtype wf, es-vartype wf, ifthenelse wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert-deq-member, bool wf, bnot wf, not wf, filter wf3, Kind-deq wf, strong-subtype-deq-subtype, strong-subtype-set3, strong-subtype-self, deq-member wf, lnk wf, tagof wf, actof wf, btrue wf, bfalse wf, es-interface-finite wf, es-interface-local wf, es-interface wf, event system wf, ma-interface wf, ma-interface-consistent wf, fpf wf, hasloc wf, decl-state wf, top wf, fpf-dom wf, id-deq wf, ma-interface-consistent-at wf, ma-abs-interface wf, es-interface-finite-implies, es-E wf, assert wf, es-is-interface wf, Id wf, es-loc wf, l member wf, Knd wf, es-kind wf |